package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class HUD {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("HUD");
		 
		 // Clocks and their guards
		 
		 tiosts.addClock("clock3");			 	 
		 
         // Variables
         TypedData modeHUD = new TypedData("modeHUD", Constants.TYPE_INTEGER);
         tiosts.addVariable(modeHUD);
         TypedData airSpeed = new TypedData("airSpeed", Constants.TYPE_INTEGER);
         tiosts.addVariable(airSpeed);
         TypedData angleOfAttack = new TypedData("angleOfAttack", Constants.TYPE_INTEGER);
         tiosts.addVariable(angleOfAttack);
         TypedData elevationHUD = new TypedData("elevationHUD", Constants.TYPE_INTEGER);
         tiosts.addVariable(elevationHUD);         
         TypedData azimuthHUD = new TypedData("azimuthHUD", Constants.TYPE_INTEGER);
         tiosts.addVariable(azimuthHUD);
         
         // Parameters
         TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(op);
         TypedData a = new TypedData("a", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(a);
         TypedData e = new TypedData("e", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(e);
         TypedData speed = new TypedData("speed", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(speed);
         TypedData angle = new TypedData("angle", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(angle);

         // Input, output, and internal actions
         
         Action init = new Action("init4", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);

         Action selectHUD = new Action("selectHUD", Constants.ACTION_INPUT);
         selectHUD.addParameter(op.getName());
         tiosts.addAction(selectHUD);
         
         Action reticlePositionHUDIn = new Action("reticlePositionHUD", Constants.ACTION_INPUT);
         reticlePositionHUDIn.addParameter(a.getName());
         reticlePositionHUDIn.addParameter(e.getName());
         tiosts.addAction(reticlePositionHUDIn);
         
         Action printReticle = new Action("printReticle", Constants.ACTION_OUTPUT);
         printReticle.addParameter(a.getName());
         printReticle.addParameter(e.getName());
         tiosts.addAction(printReticle);
         
         Action printUpdate = new Action("printUpdate", Constants.ACTION_OUTPUT);
         printUpdate.addParameter(speed.getName());
         printUpdate.addParameter(angle.getName());
         tiosts.addAction(printUpdate);
         
         Action update = new Action("update", Constants.ACTION_INPUT);
         update.addParameter(speed.getName());
         update.addParameter(angle.getName());
         tiosts.addAction(update);
                           
         // Locations
         Location start = new Location("Start4");
         tiosts.addLocation(start);
         Location S30 = new Location("S30");
         tiosts.addLocation(S30);
         Location S31 = new Location("S31");
         tiosts.addLocation(S31);     
         Location S32 = new Location("S32");
         tiosts.addLocation(S32);
         Location S33 = new Location("S33");
         tiosts.addLocation(S33);
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         
         tiosts.createTransition("Start4", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S30");
         tiosts.createTransition("S30", Constants.GUARD_TRUE, Constants.GUARD_TRUE, selectHUD, "modeHUD := op", null, "S31");
         //airToGroud assumes 6
         tiosts.createTransition("S31", "modeHUD = 6", "clock3 = 46", reticlePositionHUDIn, "azimuthHUD := a| elevationHUD := e", "clock3 := clock3 + 6", "S32");
         tiosts.createTransition("S32", "azimuthHUD = a AND elevationHUD = e", Constants.GUARD_TRUE, printReticle, null, "clock3 := 0", "S30");
         //CCIP assumes 7
         tiosts.createTransition("S31", "modeHUD = 7", Constants.GUARD_TRUE, update, "airSpeed := speed | angleOfAttack := angle", "clock3 := clock3 + 6", "S33");
         tiosts.createTransition("S33", "speed = airSpeed AND angle = angleOfAttack", Constants.GUARD_TRUE, printUpdate, null, "clock3 := 0", "S30");
         
         return tiosts;
		 
	 }

}
